#!/usr/bin/perl -w

# Copyright (C) 2010, 2011  Cesar Rodriguez <cesar.rodriguez@lsv.ens-cachan.fr>
#
# This program is free software: you can redistribute it and/or modify it
# under the terms of the GNU General Public License as published by the Free
# Software Foundation, either version 3 of the License, or any later version.
#
# This program is distributed in the hope that it will be useful, but WITHOUT
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
# FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License for
# more details.
#
# You should have received a copy of the GNU General Public License along with
# this program.  If not, see <http://www.gnu.org/licenses/>.

use strict;
use vars qw (@places %label %in %out %indeg @cut0 %cutofft %cutoffh);
use vars qw (%reach %markings);

sub debug {
	#print STDOUT @_, "\n";
}

sub build_cut0 {
	my %init = %{$_[0]};

	# if autodetect has been requested, append to %m0 all places with no
	# incoming arcs
	if ($init{"autodetect"}) {
		delete $init{"autodetect"};
		for (@places) {
			$init{$_} = 1 unless $indeg{$_};
		}
	}

	# get the keys of init hash
	@cut0 = keys %init;

	debug "Using initial marking: '@cut0'"; 
}

sub read_net {
	my ($file) = @_;
	my %hplaces;
	my %init;
	my $h;
	my @hl;
	my $hid;
	my $p;
	my $t;
	my $lbl;
	my $pnr;
	my $enr;

	open FD, '<', $file or die "'$file': $!";
	while (<FD>) {

		# match the autodetect comment generated by net2dot tool
		$init{"autodetect"} = 1 if /\* autodetect initial marking \*/;

		# parse cutoff histories in contextual unfoldings
		if (/^\s+\*(h\d+)\s+\d+\s+\d+\s+(.*) <br align/) {
			$h = $2;
			$hid = $1;
			$h =~ s/(, ){0,1}e0:_t0_//;
			@hl = split (", ", $h);
			$cutoffh{$hid} = \@hl;
			debug "file $file cutoff history $hid contents '@hl'";
		}

		# while parsing events, conditions and cutoffs, skip e0
		next if /\be0\b/;

		# place -> transition
		if (/^\s*([cp]\d*)\s*->\s*([et]\d*)/) {
			($p, $t) = ($1, $2);
			debug "file $file edge p>t $p > $t";
			$hplaces{$p} = 1;
			$indeg{$t}++;
			push @{$out{$p}}, ($t);
			push (@{$in{$t}}, ($p)) unless /arrowhead=none/;
		}

		# transition -> place
		if (/^\s*([et]\d*)\s*->\s*([cp]\d*);/) {
			($t, $p) = ($1, $2);
			debug "file $file edge t>p $t > $p";
			$hplaces{$p} = 1;
			$indeg{$p}++;
			push @{$out{$t}}, ($p);
			push @{$in{$p}}, ($t);
		}

		# label of a place
		if (/^\s*([cp]\d*)\s*.label="([^ :"]*)/) {
			($p, $lbl) = ($1, $2);
			debug "file $file p $p label $lbl";
			$hplaces{$p} = 1;
			$label{$p} = $lbl;
			$init{$p} = 1 if (/\* initial \*/);
		}

		# label of a transition
		if (/^\s*([et]\d*)\s*.label="([^ :"]*)/) {
			debug "file $file t $1 label $2";
			$label{$1} = $2;
		}

		# transition (event) is a cutoff
		if (/^\s*(e\d*)\s.*shape=Msquare/) {
			$cutofft{$1} = 1;
			debug "file $file t $1 is a cutoff";
		}
	}
	close FD;

	# build the list of places in the net
	@places = keys %hplaces;

	# and print the number of places, transitions read
	$pnr = @places;
	$enr = (keys %label) - $pnr;
	print "Net at '$file';  $enr transitions/events, $pnr " .
			"places/conditions";
	print " (autodetecting initial marking)" if $init{"autodetect"};
	print "\n";

	die "Error: No transitions read, sure about file format?" unless $enr;

	# build the initial marking
	build_cut0 \%init;
}

sub cut2labeling {
	my @cut = @_;

	# returns the marking string associated to a list of conditions
	# (places)

	return join (" ", sort (map {$label{$_}} @cut));
}

sub cut2key {
	my @cut = @_;

	return join ("_", sort @cut);
}

sub trans2labeling {
	my @trans = @_;
	return join (" ", (map {"$_:$label{$_}"} @trans));
}

sub enabled {
	my @cut = @_;
	my @fire;
	my $p;
	my $t;
	my %i;

	# get a copy of the in-degre hash table
	%i = %indeg;

	# for each place, decrement the transitions in its postset
	for $p (@cut) {
		next unless defined($out{$p});
		for $t (@{$out{$p}}) {
			$i{$t}--;
			push @fire, ($t) if $i{$t} == 0;
		}
	}
	return @fire;
}

sub fire {
	my @cut = @{$_[0]};
	my $t = $_[1];

	my %h;
	my $p;

	# build a hash table using the cut
	$h{$_} = 1 for @cut;

	# unmark preset
	for $p (@{$in{$t}}) {
		delete $h{$p};
	}

	# mark postset
	for $p (@{$out{$t}}) {
		if (defined $h{$p}) {
			print "Network is not safe!!\n";
			exit 1;
		}
		$h{$p} = 1;
	}

	# keys of hash %h conform the new marking
	return keys %h;
}

sub reach {
	my @work;
	my $m;
	my $nm;
	my @cut;
	my @ncut;
	my @ena;
	my $t;
	my $i;
	my $l;
	my $s;

	# populate the work set and the reach hash table with the initial cut
	push @work, \@cut0;
	$m = cut2key @cut0;
	$reach{$m} = ["00000"];
	$i = 1;
	debug "Cut0: @cut0 -> $m";

	# while we have a cut to explore
	while ($#work >= 0) {

		# get a cut, build its marking and get its configuration (list
		# of transitions/events)
		@cut = @{shift @work};
		$m = cut2key @cut;
		debug "Processing cut @cut, key $m (still ", $#work + 1, ")";

		# get a list of transitions enabled at this cut
		@ena = enabled @cut;
		debug " enabled: @ena";

		# fire each transition and use the new cut if not already seen
		for $t (@ena) {
			@ncut = fire (\@cut, $t);
			$nm = cut2key @ncut;
			debug " fired $t, gives cut @ncut";
			if (! defined ($reach{$nm})) {
				$s = sprintf "%05d", $i++;
				$l = @{$reach{$m}} - 1;
				$reach{$nm} = [$s, @{$reach{$m}}[1 .. $l], $t];
				debug "sequence: ", ($s, @{$reach{$m}}[1 .. $l], $t);
				push @work, [@ncut];
			} else {
				debug "  droping, already reached ",
					"by @{$reach{$nm}}";
			}
		}
	}
}

sub reach2markings {
	my $k;
	my $v;
	my $l;
	my @cut;

	while (1) {
		($k, $v) = each (%reach);
		last unless defined ($k);
		@cut = split ("_", $k);
		$l = cut2labeling @cut;
		if (defined ($markings{$l})) {
			$markings{$l} = [@$v[0], "*", @$v[1 .. @$v - 1]];
		} else {
			$markings{$l} = $v;
		}
	}
}

sub history_of {
	my ($ref, $t) = @_;
	my %exec;
	my %h = ();
	my @work; 
	my @candidates;
	my $p;
	my $k;
	my $v;
	my $found;

	debug "transition $t";
	debug "execution ", @$ref;

	# build a hash out of the execution
	$exec{$_} = 1 for (@$ref);

	@work = ($t);
	while ($#work >= 0) {
		$t = shift @work;
		if (defined $h{$t}) {
			debug "skiping $t";
			next;
		}
		$h{$t} = 1;
		debug "exploring $t";

		# compute transitions in direct asymmetric conflict to $t
		@candidates = ();
		for $p (@{$in{$t}}) {
			debug "$p:$label{$p} is in in{$t}, taking out{$p}";
			push @candidates, @{$out{$p}};
		}
		for $k (keys %out) {
			$v = $out{$k};
			$found = 0;
			for (@$v) {
				$found = 1 if ($t eq $_);
			}
			debug ("found $t in ($k, (@$v)) in out, taking in{$k}") if ($found);
			if ($found && defined ($in{$k})) {
				push (@candidates, @{$in{$k}});
			}
		}
		debug "candidates @candidates";

		# we retain those that belong to the given execution
		for (@candidates) {
			if (defined $exec{$_}) {
				push @work, ($_);
				debug "retaining $_";
			}
		}
	}

	# keys of hash %h conform the history of $t in $exec
	return keys %h;
}

sub print_markings {
	my $k;
	my $v;
	my $i;

	# we may have added transition "*" to the list of transitions
	$label{"*"} = "*";

	$i = 0;
	for $k (sort (keys %markings)) {
		$v = $markings{$k};
		#print @$v[0], " $k  after ", trans2labeling (@$v[1 .. @$v - 1]), "\n";
		print "$k\n";
		$i++;
	}
	print " -- $i markings\n"
}

sub print_histories {
	my $k;
	my $v;
	my $id;
	my $ev;
	my @h;

	$id = 5702;
	$ev = "e93";

	for $k (sort (keys %markings)) {
		$v = $markings{$k};
		last if (@$v[0] == $id);
	}

	$v = [@$v[1 .. @$v - 1]];
	@h = history_of $v, $ev;
	print "\nHistory of $ev:$label{$ev} in run $id is: \n";
	print "Run: ", trans2labeling (@$v), "\n";
	print "History: ", trans2labeling (@h), "\n";
}

sub test {
	my $e;
	my @a = ("uno", "dos", "tres", "cuatro", "cinco", "seis", "siete",
	"ocho");
	
	for $e (@a[1 .. $#a]) {
		print "$e ";
	}
	print "\n";
}

sub main {
	if (@ARGV != 1) {
		print "Usage: rs.pl DOTFILE\n";
		exit 1;
	}
	read_net $ARGV[0];
	reach ();
	reach2markings ();
	print_markings ();
	#print_histories ();
}

main ();

